$\forall$$T$:Type, $l_{1}$,$l_{2}$:($T$ List). iseg($T$; $l_{1}$; $l_{2}$) $\in$ prop\{i:l\}